Nuprl Lemma : es-pplus_functionality_wrt_iff 0,22
es:ES, e1:E, e2:{e:E| loc(e) = loc(e1)  Id }, p,
q:({e:E| loc(e) = loc(e1)  Id }{e:E| loc(e) = loc(e1)  Id }Prop).
(a, b:{e:E| loc(e) = loc(e1)  Id }. (a  [e1, e2])  (b  [e1, e2])  (p(a,b)  q(a,b)))
 ([e1,e2]~([a,b].p(a,b))+  [e1,e2]~([a,b].q(a,b))+) 
latex

DefinitionsP  Q, t  T, x(s1,s2), x:A. B(x), P  Q, [e, e'], E, (x  l), Prop, loc(e), Id, [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), [e1,e2]~([a,b].p(a;b))+, ES
Lemmases-pstar-q functionality wrt iff, event system wf, Id wf, es-loc wf, l member wf, es-E wf, es-interval wf, iff wf

origin